;;;============================================================
;;;
;;; Subject: Some questions used in binary
;;;         
;;;
;;;------------------------------------------------------------
;;;
;;; Jónathan Heras Vicente
;;; Beginning date: 29-10-09
;;;
;;;============================================================

#| To certify this book:

(certify-book "binary-remove-zeros" 0 nil)

|#

(in-package "ACL2")

(include-book "dg-binary")

(include-book "dg-list")

(set-verify-guards-eagerness 0)

;;;------------------------------------------------------------
;;; This functions are to delete the final zeros when we apply
;;; the face operator in a binary list
;;; quasi-dgb-p a list with 0's and 1's (a binary list)


(defun quasi-dgb-p (dgb)
  (if (endp dgb)
      (equal dgb nil)
    (and (or (eql (car dgb) 0)
	     (eql (car dgb) 1))
	 (quasi-dgb-p (cdr dgb)))))

;; remove the initial zeros of a list

(defun remove-initial-zeros (dgb)
  (if (endp dgb)
      nil
    (if (eql (car dgb) 0)
	(remove-initial-zeros (cdr dgb))
      dgb)))

;; reverse a list

(defun my-reverse (dgop)
  (cond ((endp dgop) nil)
	(t (append (my-reverse (cdr dgop)) (list (car dgop))))))
	   

;; my-reverse is reflexive

(defthm reverse-reverse
  (implies (true-listp x)
	   (equal (my-reverse (my-reverse x)) x))
)



(defthm append-nil
  (implies (true-listp y)
	   (equal y (append y nil)))
  :rule-classes nil)


(defthm true-listp-my-reverse
  (implies (true-listp y)
	   (true-listp (my-reverse y)))
  )


(defthm append-append
  (implies (and (true-listp x)
		(true-listp y)
		(true-listp z))
	   (equal (append (append x y) z)
		  (append x y z))))


(defthm reverse-append
  (implies (and (true-listp x) (true-listp y))
	   (equal (my-reverse (append x y))
		  (append (my-reverse y) (my-reverse x))))
:hints (("Subgoal *1/1'''" :do-not-induct t
	 :use ((:instance true-listp-my-reverse (y y))
	       (:instance append-nil (y (my-reverse y)))))))


;; If we reverse a list with car eql 1 then the last element is 1

(defthm car-reverse-last
  (implies (and (true-listp dgop) (eql (car dgop) 1))
	   (eql (car (last (my-reverse dgop))) 1)))


(defthm car-reverse-last-quasi-dgb-p
  (implies (and (quasi-dgb-p dgop) (eql (car dgop) 1))
	   (eql (car (last (my-reverse dgop))) 1)))


(defthm quasi-and-last
  (implies (and (quasi-dgb-p dgop)
		(eql (car (last dgop)) 1))
	   (dgb-p dgop)))


(defthm quasi-dgb-p-true-listp
  (implies (quasi-dgb-p dgb)
	   (true-listp dgb)))

(defthm dgb-p-true-listp
  (implies (dgb-p dgb)
	   (true-listp dgb)))


(defthm car-remove-initial-zeros
  (implies (quasi-dgb-p dgop)
	   (or (equal (remove-initial-zeros dgop)  nil)
	       (eql (car (remove-initial-zeros dgop)) 1)))
:rule-classes nil)

(defthm reverse-remove-initial-quasi-dgb-is-dgb
  (implies (quasi-dgb-p dgb)
	   (dgb-p (my-reverse (remove-initial-zeros dgb)))))



(defun remove-final-zeros (dgb)
  (my-reverse (remove-initial-zeros (my-reverse dgb))))


(defthm car-my-reverse-if-dgb-p
  (implies (and (consp dgop) (dgb-p dgop))
	   (eql (car (my-reverse dgop))
		1)))

(defthm car=1-implies-remove-initial=
  (implies (and (consp dgop) 
		(dgb-p dgop)
		(eql (car dgop) 1))
	   (equal (remove-initial-zeros dgop)
		  dgop)))  


(defthm equal-initial-and-final-if-dgb-p
  (implies (and (consp dgop) (dgb-p dgop))
	   (equal (remove-final-zeros dgop)
		  dgop)))

(defthm dgb-p-my-reverse
  (implies (quasi-dgb-p dgb)
	   (quasi-dgb-p (my-reverse dgb))))


(defthm quasi-dgb-to-dgb
  (implies (quasi-dgb-p dgb)
	   (dgb-p (remove-final-zeros dgb)))) 


(defthm last-reverse-car
  (implies (and (true-listp dgop) (eql (car (last dgop)) 1))
	   (eql (car (my-reverse dgop)) 1)))

(defthm last-reverse-car-quasi-dgb-p
  (implies (and (quasi-dgb-p dgop) (eql (car (last dgop)) 1))
	   (eql (car (my-reverse dgop)) 1)))


(defthm remove-initial-last-last
  (implies (and (consp dgop)
		(equal (car (last dgop)) 1)
		(quasi-dgb-p dgop))
	   (equal (car (last (remove-final-zeros dgop))) 1)))



(defthm car-dgop=1-implies-car-remove-final=1-aux
  (implies (and (consp dgop)
		(equal (car dgop) 1)
		(quasi-dgb-p dgop))
	   (equal (car (last (remove-initial-zeros (my-reverse
						    dgop)))) 1)))


(defthm quasi-dgb-p-remove-initial-zeros
  (implies (quasi-dgb-p dgop)
	   (quasi-dgb-p (remove-initial-zeros (my-reverse
						    dgop)))))


(defthm car-dgop=1-implies-car-remove-final=1
  (implies (and (consp dgop)
		(equal (car dgop) 1)
		(quasi-dgb-p dgop))
	   (equal (car (my-reverse (remove-initial-zeros (my-reverse
						    dgop)))) 1))
:hints (("Goal" :do-not-induct t
	 :use ((:instance car-dgop=1-implies-car-remove-final=1-aux (dgop dgop))
	       (:instance last-reverse-car-quasi-dgb-p
			   (dgop (remove-initial-zeros 
				  (my-reverse dgop)))))))
)

(defthm car-dgop=1-implies-car-remove-final-zeros=1
  (implies (and (consp dgop)
		(equal (car dgop) 1)
		(quasi-dgb-p dgop))
	   (equal (car (remove-final-zeros dgop)) 1))
)


(defthm remove-initial-zeros-append-1
  (implies (quasi-dgb-p dgop)
	   (equal (remove-initial-zeros (append dgop '(1)))
		  (append (remove-initial-zeros dgop) '(1)))))



(defthm dgb->dgl-remove-final-zeros-help-1/5-aux1
  (implies (and (consp dgop)
		(eql (car dgop) 1)
		(quasi-dgb-p dgop))
	   (equal (remove-final-zeros dgop)
		  (append '(1) (remove-final-zeros (cdr dgop)))
		  )))

(defthm dgb->dgl-remove-final-zeros-help-1/5
  (implies (and (consp dgop)
		(eql (car dgop) 1)
		(quasi-dgb-p dgop)
		(equal (dgb->dgl (cdr dgop))
		       (dgb->dgl (remove-final-zeros (cdr dgop))))
		)
	   (equal (dgb->dgl dgop)
		  (dgb->dgl (remove-final-zeros dgop)))))
 


(defun all-zeros-p (dgb)
  (if (endp dgb)
      (equal dgb nil)
    (and (eql (car dgb) 0)
	 (all-zeros-p (cdr dgb)))))


(defthm remove-initial-zeros-append-0/1-a
  (implies (and (quasi-dgb-p dgop)
		(all-zeros-p dgop))
	   (equal (dgb->dgl dgop)
		  nil)))


(defthm remove-initial-zeros-append-0/1-b
  (implies (and (quasi-dgb-p dgop)
		(all-zeros-p dgop))
	   (equal (remove-final-zeros dgop)
		  nil
		  )))

(defthm remove-initial-zeros-append-0/1'
  (implies (equal dgop nil)
	   (equal (dgb->dgl dgop)
		  nil
		  ))
:rule-classes nil)


(defthm remove-initial-zeros-append-0-1
  (implies (and (quasi-dgb-p dgop)
		(all-zeros-p dgop))
	   (equal (dgb->dgl dgop)
		  (dgb->dgl (remove-final-zeros dgop))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance remove-initial-zeros-append-0/1-a)
	       (:instance remove-initial-zeros-append-0/1-b)
	       ))))

		  
(defthm remove-initial-zeros-append-0
  (implies (and (quasi-dgb-p dgop)
		(not (all-zeros-p dgop)))
	   (equal (remove-initial-zeros (append dgop '(0)))
		  (append (remove-initial-zeros dgop) '(0)))))



(defthm quasi-implies-cdr-quasi
  (implies (quasi-dgb-p dgop)
	   (quasi-dgb-p (cdr dgop))))


(defthm dgb->dgl-remove-final-zeros-help-1/3-aux1
  (implies (and (consp dgop)
		(eql (car dgop) 0)
		(quasi-dgb-p dgop)
		(not (all-zeros-p (cdr dgop))))
	   (equal (remove-final-zeros dgop)
		  (my-reverse (remove-initial-zeros
			       (append (my-reverse (cdr dgop))
				       '(0))))
		  )))


(defthm not-all-zeros-append-a
  (implies (quasi-dgb-p dgop)
	   (not (all-zeros-p (append dgop '(1))))))

(defthm not-all-zeros-append-b
  (implies (and (quasi-dgb-p dgop)
		(not (all-zeros-p dgop)))
	   (not (all-zeros-p (append dgop '(0))))))

(defthm not-all-zeros-implies-reverse-not-all-zeros
  (implies (and (quasi-dgb-p dgop)
		(not (all-zeros-p dgop)))
	   (not (all-zeros-p (my-reverse dgop)))))

(defthm dgb->dgl-remove-final-zeros-help-1/3-aux2
  (implies (and (consp dgop)
		(eql (car dgop) 0)
		(quasi-dgb-p dgop)
		(not (all-zeros-p (cdr dgop))))
	   (equal (remove-final-zeros dgop)
		  (my-reverse (append (remove-initial-zeros 
				       (my-reverse (cdr dgop)))
				       '(0))))
		  ))


(defthm dgb->dgl-remove-final-zeros-help-1/3-aux3
  (implies (and (consp dgop)
		(eql (car dgop) 0)
		(quasi-dgb-p dgop)
		(not (all-zeros-p (cdr dgop))))
	   (equal (remove-final-zeros dgop)
		  (append '(0) (remove-final-zeros (cdr dgop)))
		  )))


(defthm car=0-and-cdr-all-zeros-implies-all-zeros
  (implies (and (consp dgop)
		(eql (car dgop) 0)
		(all-zeros-p (cdr dgop)))
	   (all-zeros-p dgop)))

	
(defthm dgb->dgl-remove-final-zeros-help-1/3-a
  (implies (and (consp dgop)
		(eql (car dgop) 0)
		(quasi-dgb-p dgop)
		(equal (dgb->dgl (cdr dgop))
		       (dgb->dgl (remove-final-zeros (cdr dgop))))
		(all-zeros-p (cdr dgop))
		)
	   (equal (dgb->dgl dgop)
		  (dgb->dgl (remove-final-zeros dgop))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance car=0-and-cdr-all-zeros-implies-all-zeros)
	       (:instance remove-initial-zeros-append-0-1)))))


(defthm dgb->dgl-remove-final-zeros-help-1/3-b
  (implies (and (consp dgop)
		(eql (car dgop) 0)
		(quasi-dgb-p dgop)
		(equal (dgb->dgl (cdr dgop))
		       (dgb->dgl (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p (cdr dgop)))
		)
	   (equal (dgb->dgl dgop)
		  (dgb->dgl (remove-final-zeros dgop)))))

(defthm dgb->dgl-remove-final-zeros-help-1/3
  (implies (and (consp dgop)
		(eql (car dgop) 0)
		(quasi-dgb-p dgop)
		(equal (dgb->dgl (cdr dgop))
		       (dgb->dgl (remove-final-zeros (cdr dgop))))
		)
	   (equal (dgb->dgl dgop)
		  (dgb->dgl (remove-final-zeros dgop))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance dgb->dgl-remove-final-zeros-help-1/3-a)
	       (:instance dgb->dgl-remove-final-zeros-help-1/3-b))))
)

(defthm dgb->dgl-remove-final-zeros
  (implies (quasi-dgb-p dgop)
	   (equal (dgb->dgl dgop)
		  (dgb->dgl (remove-final-zeros dgop))))
)


;;;-------------------------------------------------------------

(defun reverse-cdr (ls)
  (if (endp (cdr ls))
      nil
    (cons (car ls) (reverse-cdr (cdr ls)))))




